(set-logic AUFNIRA)
(set-option :smt.ematching false)
(set-option :rewriter.ite_extra_rules true)
(declare-const x Int)
(assert (> x 0))
(check-sat)
(exit)

(declare-datatypes ((Nat 0)) (((succ (pred Nat)) (zero))))
(declare-datatypes ((Lst 0)) (((Nil))))
(declare-fun minus (Nat Nat) Nat)
(declare-fun nat-to-int (Nat) Int)
(declare-fun drop (Nat Lst) Lst)
(declare-fun take (Nat Lst) Lst)
(assert (forall ((x Nat) (y Nat)) (=> (= 0 (nat-to-int y)) (= x y))))
(assert (forall ((x Nat) (y Nat)) (= (nat-to-int (minus x y)) (ite (< 0 0) 0 (- 0 (nat-to-int y))))))
(assert (not (forall ((n Nat) (m Nat) (xs Lst)) (= (drop n (take m xs)) (take (minus m n) (drop n xs))))))
(check-sat)